the_es:ES, e:E. isrcv(e)  emsg(e)  Msg 

latex

Definitions	False, t  T, x:A. B(x), P  Q, True, f(a), tag(k), lnk(k), act(k), islocal(k), b, kindcase(k; a.f(a); l,t.g(l;t) ), isrcv(k), x:AB(x), left+right, Knd, x:AB(x), s = t, Type, msg(l;t;v), P & Q, es_info(es), es_val(es), kind(e), val(e), tag(e), lnk(e), es-M(es), emsg(e), Msg, isrcv(e), E, ES, kind(e)
Lemmas	event system wf, msg wf, lnk wf, tagof wf, assert wf, isrcv wf, kind wf, Knd wf, subtype rel self, true wf, false wf